using System;
using System.IO;
using System.Text;
using ExternalLib;
using ExternalLib2;
using FieldAccessExtractor;
using Microsoft.Pex.Framework;
using Covana.CoverageExtractor;
using Covana.ResultTrackingExtrator;


namespace Benchmarks
{
    public class Father : TestInterface
    {
        private int money;

        private Child child;

        private string Name = "name";

        public Father(int money)
        {
            this.money = money;
        }

        private Wife wife;
        private bool isHappy;
        private int value;

        public void Marry()
        {
            wife = new Wife();
        }

        public void MakeWifeHappy()
        {
            if (wife != null)
            {
                wife.Happiness = 5;
            }
        }


        public void SetMoney(int value)
        {
            money = value;
        }

        public void SetChild(Child value)
        {
            child = value;
        }

        public bool IsChildGood()
        {
            isHappy = child.IsLargerThanFive();
            if (isHappy)
            {
                return true;
            }
            return false;
        }

        public bool IsSelfGood()
        {
            bool b = child.IsLargerThanFive();
            if (wife != null && wife.Happiness > 5)
            {
                return true;
            }
            return false;
        }

        public void SetName(string name)
        {
            this.Name = name;
        }

        public string GetName()
        {
            return Name;
        }

        public void SetValue(int i)
        {
            value = i;
        }

        public int GetValue()
        {
            return value;
        }

        public static void External_Method_Wrapper(Child child)
        {
            child.ThrowException();
        }

        public static void DoNothing()
        {
            return;
        }
    }

    public class Wife
    {
        private int happiness;

        public int Happiness
        {
            get { return happiness; }
            set { happiness = value; }
        }
    }


    [PexClass(typeof (Test2))]
    [ResultTrackingObserver]
    public partial class Test2
    {
        [PexMethod]
        public void Testchangename([PexAssumeNotNull] Father p, Child child, string s)
        {
            child.ChangeName(p);
            if (p.GetName() == "changehello")
            {
                Console.WriteLine("hi");
            }

//            p.SetName(s);
            if (p.GetName() == "kkk")
            {
                Console.WriteLine("hihi");
            }

            Console.WriteLine("end");
        }

        [PexMethod]
        public void Testchangevalue([PexAssumeNotNull] Father p, Child child, string s)
        {
            child.ChangeValue(p);
            if (p.GetValue() == 1)
            {
                Console.WriteLine("hi");
            }
            if (p.GetValue() == 2)
            {
                Console.WriteLine("hi2");
            }
            Console.WriteLine("end");
        }
    }

    [PexClass(typeof (Father))]
    [InsufficientObjectFactoryObserver]
    [FieldAccessObserver]
    [ResultTrackingObserver]
    public partial class UninstrumentedTest
    {
        [PexMethod]
        public void TestUninstrumentedMethod1([PexAssumeUnderTest] Father p, Child child)
        {
            p.SetChild(child);
            p.IsChildGood();
        }

        [PexMethod]
        public void ExternalMethodException([PexAssumeUnderTest] Father p, [PexAssumeNotNull]Child child)
        {
            Father.DoNothing();
//            Father.External_Method_Wrapper(child);
            child.ThrowException();
            Console.WriteLine("reach");
        }

        [PexMethod]
        public void TestChild(Child child, [PexAssumeNotNull] int[] a)
        {
            PexAssume.IsTrue(a.Length > 1);
            child.Format(a);
            if (a[0] > 100)
            {
                Console.WriteLine("a[1] != null");
            }
            else
            {
                Console.WriteLine("a[1] == null");
            }


            Console.WriteLine("end");
        }

        [PexMethod]
        public void TestUninstrumentedMethod2([PexAssumeUnderTest] Father p)
        {
            p.IsSelfGood();
        }

//        [PexMethod]
        public void ExternalMethodException()
        {
            File.WriteAllBytes("f://out.txt", new byte[0]);
            var array = File.ReadAllBytes("f://out.txt");
            var size = array.Length;
            if (size != 0)
            {
                Console.WriteLine("hi");
            }
        }

        [PexMethod]
        public void UninstrumentedBenchmark1(string file, int y)
        {
            string status = File.ReadAllText(file);
            if (status == "OK")
            {
                int value = ExternalObj.Compute(y);
                Console.Out.WriteLine("value is: " + value);
                if (value > 5)
                {
                    Console.WriteLine("hit!");
                }
            }

            PexObserve.Value("status", status);
        }


        [PexMethod]
        public void UninstrumentedBenchmark2(int y)
        {
            string path = "f://out.txt";
            File.WriteAllBytes(path, new ASCIIEncoding().GetBytes("OK"));

            if (File.ReadAllText(path) == "OK")
            {
                int value = ExternalObj.Compute(y);
                Console.Out.WriteLine("value is: " + value);
                if (value > 5)
                {
                    Console.WriteLine("hit!");
                }
            }
        }
    }
}